Nuprl Lemma : not_over_or
13,42
postcript
pdf
A
,
B
:
. (
(
A
B
))
((
A
) & (
B
))
latex
Up
core
2
,
core
2
Definitions
t
T
,
P
Q
,
P
Q
,
P
&
Q
,
P
Q
,
P
Q
,
,
x
:
A
.
B
(
x
)
,
A
,
False
Lemmas
not
wf
origin
A, B:
. (
(A 
B)) 
((A) & (B)) A, B:. ((A B)) ((A) & (B)) 
T Q Q Q Qx:A. B(x)A